Incremental version of the solver #1000

Stevendeo · 2023-12-04T16:07:01Z

The target of this PR: the first part before getting rid of the Commands module. As the legacy frontend still relies on it, this PR only cuts all the dependencies of the dolmen loop (solving_loop.ml)

Stevendeo · 2023-12-07T16:44:11Z

src/lib/reasoners/satml_frontend.ml

@@ -1303,7 +1303,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct

  let assume env gf _dep =
    (* dep currently not used. No unsat-cores in satML yet *)
-    assert (SAT.decision_level env.satml == 0);
+    (* assert (SAT.decision_level env.satml == 0); *)


I commented these assertions because one test failed and I forgot to put them back; the test ./alt-ergo -o smtlib2 --prelude tests/cram.t/prelude.ae tests/cram.t/postlude.smt2 still fails because of it

Yeah because there are push'd level now. We should probably be able to expose the "push level" and check that instead (i.e. assertion that the decision level is equal to the length of the increm_guard). Probably as a SAT.can_assume env.satml check or some such.

Would it be correct not to assert at the decision level 0, but at decision_level env?

expose the "push level"

Both my solution and yours may be incorrect actually.

(assert f) ; decision level = 0, push level = 0 (push 42) ; decision level = 0, push level = 42 (check-sat)

Maybe a counter for every query?

Yeah I realized that after (because for the first check-sat it will be 0 as it used to be). The correct test I believe is decision_level <= push_level (to also capture both (check-sat)(push)(check-sat) and (push)(check-sat)(pop)(check-sat)).

Here's another solution: at the end of a query, keep track of the current decision level and set it as the latest known decision level on the satml_frontend side. I find it hard to justify keeping the invariant decision_level <= push_level for a consistency check (in other words, if we ever raise this assertion during a pr, I'm not sure how relevant it would be for debugging).

I find it hard to justify keeping the invariant decision_level <= push_level for a consistency check (in other words, if we ever raise this assertion during a pr, I'm not sure how relevant it would be for debugging).

This is not just a consistency check; I am not sure the solver will do the right thing in this case. In particular, I am not sure the assumed assertions cannot be forgotten upon later backtracking — in fact, I am pretty sure they will be forgotten (partially) for the default CDCL-Tableaux solver given my current understanding of lazy_cnf.

(Note that for decisions level between 0 and push_level forgetting assumptions upon backtracking is OK because that is exactly the semantics we want for push and pop)

src/bin/common/solving_loop.ml

tests/cram.t/prelude.ae

Halbaroth · 2023-12-08T08:36:30Z

src/lib/reasoners/satml_frontend.ml

-    assert (SAT.decision_level env.satml == 0);
-    try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf])
+
+    try ignore (assume_aux ~dec_lvl:(SAT.decision_level env.satml) env [add_guard env gf])


We should benchmark this PR to be sure this modification is ok :)

src/bin/common/solving_loop.ml

bclement-ocp · 2023-12-11T09:18:40Z

src/lib/reasoners/fun_sat.ml

-    if Options.get_tableaux_cdcl () then
-      Errors.run_error
-        (Errors.Unsupported_feature
-           "Incremental commands are not implemented in \
-            Tableaux(CDCL) solver ! \
-            Please use the Tableaux or CDLC SAT solvers instead"
-        );


I thought this was still not working — just commenting here to make sure we don't merge until either this works with Tableaux(CDCL) (probably not worth it, waiting on @Halbaroth investigation whether we should remove Tableaux(CDCL)) or to keep the assert back in.

src/lib/frontend/d_cnf.mli

src/lib/reasoners/fun_sat_frontend.ml

bclement-ocp · 2023-12-11T09:25:25Z

Looks like there are conflict, rebase would be appreciated :)

Stevendeo · 2023-12-12T13:40:49Z

I'm not sure why, but the tests do not pass on the CI, but make runtest-ci do work on my side.

bclement-ocp · 2023-12-12T14:38:01Z

I'm not sure why, but the tests do not pass on the CI, but make runtest-ci do work on my side.

Weird. I can't reproduce either. But on the CI it seems surprisingly reproducible — all runners on all OSes fail. Maybe a cache problem, somehow?

Stevendeo · 2023-12-14T09:34:19Z

I'm going to push some commits to this branch to test what's wrong with the tests on the CI, please don't take them into account

Stevendeo · 2023-12-14T09:47:01Z

Here's the CI's result :

Fatal error: exception File "src/lib/reasoners/satml.ml", line 1990, characters 9-15: Assertion failed

There is no line 1990 in satml.ml...

Stevendeo · 2024-03-25T11:10:30Z

Okay I finished working on the pop-reinitialization version. What it does now is to rework all the analysis (removing the smt commands we don't want to be executed twice) when a pop occurs. I will add some documentation to explain what's going on, but at least tests are OK on my machine.

bclement-ocp · 2024-03-25T11:22:46Z

What it does now is to rework all the analysis (removing the smt commands we don't want to be executed twice) when a pop occurs

Ah so this uses a stmt list instead of command list? That sounds smart.

bclement-ocp · 2024-03-25T11:28:07Z

I will add some documentation to explain what's going on, but at least tests are OK on my machine.

You marked this as ready for review but also noted this; should I wait for that documentation to be written before doing a review or do you want a pass now?

Stevendeo · 2024-03-25T13:55:32Z

I thought I was ready modulo documentation, but as I wrote documentation I noticed a few issues remaining (cf CI). Ready for review in a minute

Stevendeo · 2024-03-25T14:07:26Z

Ready! For real this time

bclement-ocp

I did a first pass; I will do a second more thorough one later this week but there is still actionable feedback. I wish we had to extract less stuff from D_cnf but oh well.

We need to run benchmarks on both internal datasets (AE format and SMT format) in both modes, will queue them tonight

src/lib/util/options.mli

bclement-ocp · 2024-03-26T12:37:54Z

src/lib/reasoners/satml.ml

@@ -999,9 +1004,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
  let print_aux fmt hc =
    Format.fprintf fmt "%a@," Atom.pr_clause hc

+  let is_unsat env : unit = env.is_unsat <- true


Please call this function set_unsat or set_is_unsat :)

src/lib/reasoners/satml.ml

bclement-ocp · 2024-03-26T12:41:07Z

src/lib/reasoners/satml.ml

+           (* This was first added by PR 1000, but it triggers a bug in
+              tests/cc/testfile-ac_cc002.ae with option
+              --no-tableaux-cdcl-in-instantiation *)


If this code is removed then I believe the unit_tenv_queue field should also be removed (in fact I think it should be removed in any case, it was a quick-and-dirty hack to test an hypothesis if I recall — same goes for this code).

I think it was important to restore the old unit_tenv from before a push (cf Satml.pop)

I believe this should only be the case with the code below uncommented — without this code, Alt-Ergo should only ever add to unit_tenv facts that are true at level 0 (otherwise it is probably a soundness bug) which shouldn't be impacted by push/pop.

(If I recall correctly, I added this code and the unit_tenv stack because unit_tenv with the specification of only adding things known at level 0 is less useful with incremental solving and we were trying to solve the performance issues)

src/bin/common/solving_loop.ml

tests/adts/simple_1.ae

Stevendeo · 2024-04-05T16:42:07Z

I can't figure out why there is a test not working on the CI that works on my side. I guess this is because the CI is slow, but I'm not sure where the error is triggered...

bclement-ocp · 2024-04-05T19:03:22Z

I can't figure out why there is a test not working on the CI that works on my side. I guess this is because the CI is slow, but I'm not sure where the error is triggered...

The test is testfile-qfbv-timeout.dolmen.smt2 so that is probably because this PR somehow breaks the timelimit-per-goal option.

Stevendeo force-pushed the get-rid-of-cmd branch 5 times, most recently from c27098e to 432d646 Compare December 7, 2023 15:59

Stevendeo marked this pull request as ready for review December 7, 2023 16:27

Stevendeo requested review from bclement-ocp, Halbaroth and hra687261 and removed request for bclement-ocp and Halbaroth December 7, 2023 16:28

Stevendeo commented Dec 7, 2023

View reviewed changes

Halbaroth reviewed Dec 8, 2023

View reviewed changes

bclement-ocp reviewed Dec 11, 2023

View reviewed changes

Stevendeo force-pushed the get-rid-of-cmd branch 3 times, most recently from 21639c6 to 8b80218 Compare December 12, 2023 11:06

Stevendeo force-pushed the get-rid-of-cmd branch 7 times, most recently from 3ba929d to d4cd365 Compare December 14, 2023 10:56

Interleaving full imperative and partial imperative modes

2fd8303

Stevendeo force-pushed the get-rid-of-cmd branch from 2efa175 to 2fd8303 Compare March 22, 2024 17:07

Stevendeo added 2 commits March 22, 2024 18:26

Update tests

e918fa0

Reactivating abstract value printing and update tests

c985aed

Stevendeo changed the title ~~WIP: Incremental version of the solver~~ Incremental version of the solver Mar 25, 2024

Stevendeo marked this pull request as ready for review March 25, 2024 11:07

Stevendeo marked this pull request as draft March 25, 2024 11:08

Stevendeo marked this pull request as ready for review March 25, 2024 11:08

Stevendeo added 3 commits March 25, 2024 12:30

Documentation and small fix

0f0dd69

Style

c10ad82

Indent

4bbfc84

Fix for test tests/cc/testfile-ac_cc002.ae

e844f17

bclement-ocp reviewed Mar 26, 2024

View reviewed changes

Stevendeo added 5 commits March 28, 2024 11:07

Poetry

cfbc8bc

Disactivating push & pop in queries in non incremental mode

f03b2e1

Linter

baba255

Reinitializing current path to avoid double replay

e02c791

Fix timeout issues

cf3b8a2

Stevendeo force-pushed the get-rid-of-cmd branch from 9570638 to cf3b8a2 Compare April 5, 2024 15:17

Stevendeo added 3 commits April 5, 2024 17:25

Rename function

97353c0

Removing unit_tenv_queue

a91b605

Fix for another issue I need to test my PR

a0f518e

Stevendeo force-pushed the get-rid-of-cmd branch from 9955e61 to a0f518e Compare April 5, 2024 16:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Incremental version of the solver #1000

Incremental version of the solver #1000

Stevendeo commented Dec 4, 2023 •

edited

Loading

Stevendeo Dec 7, 2023

bclement-ocp Dec 7, 2023

Stevendeo Dec 8, 2023

Stevendeo Dec 8, 2023 •

edited

Loading

Stevendeo Dec 8, 2023

bclement-ocp Dec 8, 2023

Stevendeo Dec 11, 2023 •

edited

Loading

bclement-ocp Dec 11, 2023

bclement-ocp Dec 11, 2023

Halbaroth Dec 8, 2023

bclement-ocp Dec 11, 2023

bclement-ocp commented Dec 11, 2023

Stevendeo commented Dec 12, 2023

bclement-ocp commented Dec 12, 2023

Stevendeo commented Dec 14, 2023

Stevendeo commented Dec 14, 2023

Stevendeo commented Mar 25, 2024

bclement-ocp commented Mar 25, 2024

bclement-ocp commented Mar 25, 2024

Stevendeo commented Mar 25, 2024

Stevendeo commented Mar 25, 2024

bclement-ocp left a comment

bclement-ocp Mar 26, 2024

bclement-ocp Mar 26, 2024

Stevendeo Mar 28, 2024

bclement-ocp Mar 28, 2024

Stevendeo commented Apr 5, 2024

bclement-ocp commented Apr 5, 2024

Incremental version of the solver #1000

Are you sure you want to change the base?

Incremental version of the solver #1000

Conversation

Stevendeo commented Dec 4, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevendeo Dec 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevendeo Dec 11, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp commented Dec 11, 2023

Stevendeo commented Dec 12, 2023

bclement-ocp commented Dec 12, 2023

Stevendeo commented Dec 14, 2023

Stevendeo commented Dec 14, 2023

Stevendeo commented Mar 25, 2024

bclement-ocp commented Mar 25, 2024

bclement-ocp commented Mar 25, 2024

Stevendeo commented Mar 25, 2024

Stevendeo commented Mar 25, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevendeo commented Apr 5, 2024

bclement-ocp commented Apr 5, 2024

Stevendeo commented Dec 4, 2023 •

edited

Loading

Stevendeo Dec 8, 2023 •

edited

Loading

Stevendeo Dec 11, 2023 •

edited

Loading